\begin{tabbing}
es{-}responsive(${\it es}$;$l_{1}$;${\it tg}_{1}$;$l_{2}$;${\it tg}_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$=rcv($l_{1}$,${\it tg}_{1}$).\+\+
\\[0ex]$\exists$${\it e'}$=rcv($l_{2}$,${\it tg}_{2}$).
\\[0ex]$e$ $\leq$ sender(${\it e'}$) 
\\[0ex]\& ($\forall$$e_{2}$=rcv($l_{1}$,${\it tg}_{1}$). ($e$ $<$loc $e_{2}$) $\Rightarrow$ (sender(${\it e'}$) $<$loc $e_{2}$))
\\[0ex]\& ($\forall$${\it e''}$=rcv($l_{2}$,${\it tg}_{2}$). sender(${\it e''}$) $=$ sender(${\it e'}$) $\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$))
\-\\[0ex]\& (\=$\forall$${\it e'}$=rcv($l_{2}$,${\it tg}_{2}$).\+
\\[0ex]$\exists$$e$=rcv($l_{1}$,${\it tg}_{1}$).
\\[0ex]$e$ $\leq$ sender(${\it e'}$) 
\\[0ex]\& ($\forall$${\it e''}$=rcv($l_{2}$,${\it tg}_{2}$). (sender(${\it e''}$) $<$loc sender(${\it e'}$)) $\Rightarrow$ (sender(${\it e''}$) $<$loc $e$)))
\-\-
\end{tabbing}